Section: New Results

Security

Participants : Patrick Cousot, Radhia Cousot.

We have developed, episodically since 2007, an abstract interpretation framework for security and program securization that is the transformation of a program into a secured program satisfying security criteria defined by a human or artificial supervisor (this is verification when no transformation is needed). The securization is based on the notion of responsibility analysis determining which choices in the program (inputs, random draws, interrupts, schedules, etc.) can definitely cause or avoid desired or menacing events, or have no control at all on the occurrence of these events. Various securization policies (eager, early or late lazy, etc.) have been identified to prevent or enforce the occurrence of events.